Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Equality in iterated Sigma types #899

Merged

Conversation

maybemabeline
Copy link
Contributor

Computed some equalities in iterated Sigma types. Maybe this can be generalized some more, but this is what I currently need for my work with pushouts, where some cocone structures involve equality of a quadruple. Input on the names is welcome as usual.

@maybemabeline maybemabeline marked this pull request as ready for review November 3, 2023 09:39
Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the PR! I feel like eventually we'll want to formalize these computations in full generality with iterated sigmas, but for now it's nice to have them 👌

src/foundation-core/equivalences.lagda.md Outdated Show resolved Hide resolved
src/foundation/equality-dependent-pair-types.lagda.md Outdated Show resolved Hide resolved
src/foundation/equality-dependent-pair-types.lagda.md Outdated Show resolved Hide resolved
@maybemabeline
Copy link
Contributor Author

Regarding the coherence proof, I wasn't sure if it could be done without path induction or not.
The problem is this: when you have an equality in a Sigma type of the form Σ A (Σ B C), you can obtain an equality in the first component in two ways; either take the first component of the equality immediately, or first associate to the left and then take the first component twice.

@maybemabeline
Copy link
Contributor Author

This is everything I wanted to do with this PR, so it can be merged if the renamings are ok

@fredrik-bakke
Copy link
Collaborator

I'm not a huge fan of some of the names that are introduced in this PR, but I don't have any better suggestions. So to not hold you up, I will merge the PR in its current state. we can always change the names later anyways :)

@fredrik-bakke fredrik-bakke enabled auto-merge (squash) November 9, 2023 12:21
@fredrik-bakke fredrik-bakke merged commit 58d3041 into UniMath:master Nov 9, 2023
4 checks passed
@maybemabeline maybemabeline deleted the equality-iterated-sum-types branch November 10, 2023 08:20
@maybemabeline maybemabeline restored the equality-iterated-sum-types branch November 10, 2023 08:20
@maybemabeline maybemabeline deleted the equality-iterated-sum-types branch November 10, 2023 08:20
@maybemabeline maybemabeline restored the equality-iterated-sum-types branch November 10, 2023 08:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants